theory Least_Fixpoint imports "./Composition" "Binders.MRBNF_FP" begin typ "('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k) T1_pre" typ "('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k) T2_pre" (* 'a, 'b free 'c passive free 'd passive live 'e, 'f bound 'g bound free 'h, 'i, 'j, 'k live *) (************* DEFINITIONS *****************)